YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs:
  { and(tt(), X) -> X
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, s(M)) -> plus(x(N, M), N) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
   [and](x1, x2) = 1 + 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2
                                                     
          [tt]() = 1                                 
                                                     
  [plus](x1, x2) = x1 + 3*x2                         
                                                     
           [0]() = 0                                 
                                                     
         [s](x1) = 2 + x1                            
                                                     
     [x](x1, x2) = x1 + 2*x1*x2 + x2                 
                                                     
  
  This order satisfies the following ordering constraints.
  
     [and(tt(), X)] =  7 + 6*X            
                    >  X                  
                    =  [X]                
                                          
     [plus(N, 0())] =  N                  
                    >= N                  
                    =  [N]                
                                          
    [plus(N, s(M))] =  N + 6 + 3*M        
                    >  2 + N + 3*M        
                    =  [s(plus(N, M))]    
                                          
        [x(N, 0())] =  N                  
                    >=                    
                    =  [0()]              
                                          
       [x(N, s(M))] =  5*N + 2*N*M + 2 + M
                    >  4*N + 2*N*M + M    
                    =  [plus(x(N, M), N)] 
                                          

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { plus(N, 0()) -> N
  , x(N, 0()) -> 0() }
Weak Trs:
  { and(tt(), X) -> X
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { plus(N, 0()) -> N }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
   [and](x1, x2) = 1 + x1 + x1*x2 + x1^2 + 3*x2
                                               
          [tt]() = 2                           
                                               
  [plus](x1, x2) = 3 + x1 + 2*x2               
                                               
           [0]() = 0                           
                                               
         [s](x1) = 1 + x1                      
                                               
     [x](x1, x2) = 2*x1 + 2*x1*x2 + 2*x2 + x2^2
                                               
  
  This order satisfies the following ordering constraints.
  
     [and(tt(), X)] =  7 + 5*X                    
                    >  X                          
                    =  [X]                        
                                                  
     [plus(N, 0())] =  3 + N                      
                    >  N                          
                    =  [N]                        
                                                  
    [plus(N, s(M))] =  5 + N + 2*M                
                    >  4 + N + 2*M                
                    =  [s(plus(N, M))]            
                                                  
        [x(N, 0())] =  2*N                        
                    >=                            
                    =  [0()]                      
                                                  
       [x(N, s(M))] =  4*N + 2*N*M + 3 + 4*M + M^2
                    >= 3 + 4*N + 2*N*M + 2*M + M^2
                    =  [plus(x(N, M), N)]         
                                                  

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs: { x(N, 0()) -> 0() }
Weak Trs:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'custom shape polynomial interpretation' to
orient following rules strictly.

Trs: { x(N, 0()) -> 0() }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-restricted polynomial
  interpretation.
   [and](x1, x2) = 1 + 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2
                                                     
          [tt]() = 1                                 
                                                     
  [plus](x1, x2) = x1 + x2                           
                                                     
           [0]() = 1                                 
                                                     
         [s](x1) = 1 + x1                            
                                                     
     [x](x1, x2) = 2*x1 + x1*x2 + x2 + 2*x2^2        
                                                     
  
  This order satisfies the following ordering constraints.
  
     [and(tt(), X)] =  7 + 6*X                    
                    >  X                          
                    =  [X]                        
                                                  
     [plus(N, 0())] =  N + 1                      
                    >  N                          
                    =  [N]                        
                                                  
    [plus(N, s(M))] =  N + 1 + M                  
                    >= 1 + N + M                  
                    =  [s(plus(N, M))]            
                                                  
        [x(N, 0())] =  3*N + 3                    
                    >  1                          
                    =  [0()]                      
                                                  
       [x(N, s(M))] =  3*N + N*M + 3 + 5*M + 2*M^2
                    >  3*N + N*M + M + 2*M^2      
                    =  [plus(x(N, M), N)]         
                                                  

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { and(tt(), X) -> X
  , plus(N, 0()) -> N
  , plus(N, s(M)) -> s(plus(N, M))
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^2))